Nuprl Lemma : R-compat-disjoint 0,22
A, B:Realizer. (i:Id. (R-has-loc(A;i) & R-has-loc(B;i)))  R-icompat(A;B)  A || B 
latex

Definitionst  T, R-interface-compat(A;B), x:AB(x), Prop, True, Type, R-frame-compat(A;B), if b t else f fi, False, Knd, f || g, R-loc(R), s = t, b, , a = b, x:AB(x), P  Q, Unit, left+right, Rnone?(x1), Void, P  Q, Rplus-right(x1), Rplus-left(x1), P  Q, #$n, n-m, , {x:A| B(x) }, {T}, Rplus?(x1), a<b, , ij, -n, , R-size(R), n+m, A || B, R-icompat(A;B), P  Q, R-has-loc(R;i), b, P & Q, A, Id, x:A. B(x), AB, Realizer, , T
Lemmassquash wf, R-has-loc-base, ge wf, nat properties, nat wf, le wf, es realizer wf, Rplus? wf, R-size-decreases, R-icompat wf, R-size wf, nat plus wf, R-has-loc-Rplus, assert of bor, Rplus-left wf, R-has-loc wf, Rplus-right wf, Rnone? wf, ifthenelse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-id, eq id wf, bool wf, bnot wf, not wf, assert wf, Id wf, R-loc wf, true wf, R-interface-compat wf

origin